package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{Tru,And,Or,Formula,Flse}

trait PropositionalFormulaMaker extends AbstractFormulaMaker { 

  /**
   * <p>
   *   General version of the <code>conjunction</code> method. It needs a 
   *   <code>first</code> formula and a list of <code>atoms</code> (eventually empty)
   *   to succeed. 
   *   Create a formula that is a conjunction of the given <code>atoms</code>. 
   * </p>
   *
   * @parma first: The first atom
   * @param atoms: The list of atoms formulae to connect to the <code>first</code> atom.
   * @return     : The conjuncted formula.
   */  
  protected def conjunction(first: Formula)(atoms: List[Formula]): Formula =
    super.conjunction[Formula](first,And)(atoms)
  
  /**
   * <p>
   * 	Create a formula that is a conjunction of the given <code>atoms</code>.
   *	It calls method <code>conjunction</code> with <code>first</code> set to true
   *	(that is the neutral proposition for the conjunction - '&' - connector).  
   * </p>
   *
   * @param atoms: The list of atoms formulae.
   * @return     : The conjuncted formula.
   */  
  protected def conjunction(atoms: List[Formula]): Formula =
    conjunction(Tru)(atoms)
   
  /**
   * <p>
   *   General version of the <code>disjunction</code> method. It needs a 
   *   <code>first</code> formula and a list of <code>atoms</code> (eventually empty)
   *   to succeed. 
   *   Create a formula that is a disjointion of the given <code>atoms</code>. 
   * </p>
   *
   * @parma first: The first atom
   * @param atoms: The list of atoms formulae to connect to the <code>first</code> atom.
   * @return     : The disjointed formula.
   */      
  protected def disjunction(first: Formula)(atoms: List[Formula]): Formula = 
    super.disjunction[Formula](first,Or)(atoms)

    
  /**
   * <p>
   *	Create a formula that is a disjonction of the given <code>atoms</code>.
   *    It calls method <code>disjunction</code> with <code>first</code> set to true
   *    (that is the neutral proposition for the conjunction - '|' - connector).  
   * </p>
   *
   * @param atoms: The list of atoms formulae.
   * @return     : The disjointed formula.
   */  
  protected def disjunction(atoms: List[Formula]): Formula =
    disjunction(Flse)(atoms)
  
   
}
